$\forall$${\it es}$:ES, $A$:Type, $X$:AbsInterface($A$), $L$:(E($X$) List). $X$($L$) $\in$ ($A$ List)